;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "MThreshold.lisp")
(require "Mimage.lisp")
(require "MCommon.lisp")

(module TThreshold
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "avl-rational-keys" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  (include-book "testing" :dir :teachpacks)
  
  (import ICommon)
  (import IImage)
  (import IThreshold)
  
  (defconst *header* (list 1 2 3 4 5 6))
  (defconst *width* 2)
  (defconst *height* 2)
  (defconst *tree1* (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 *width*) -3 *height*))
  (defconst *tree2* (insertPixel *tree1* 1 2 100 100 100))
  (defconst *tree3* (insertPixel *tree2* 2 2 105 105 105))
  (defconst *tree4* (insertPixel *tree3* 1 1 110 110 110))
  (defconst *tree5* (insertPixel *tree4* 2 1 115 115 115))
  
  (check-expect (pixelLessThanThreshold '(20 22 23) '(21 23 24)) t)
  (check-expect (car (getPixel (processThreshold *tree5* (createRGB 108 108 108) 1 *height* *width* *height*) 2 2)) 255)
  (check-expect (car (getPixel ( MainThreshold *tree5* 109 109 109) 1 2)) 255)
  
  
  ;this function takes a base and a number, converts the number to the representative base given and checks 
  ;that the returned list has elements that are all less than the base.
  (defproperty test-pixelLessThanThreshold :repeat 1000
    (a :value (random-integer)
       :where (< a 100)
       b :value (random-integer)
         :where (< b 100)
         c :value (random-integer)
           :where (< c 100))
    (let ((pixel (createRGB a b c))
          (threshOld (createRGB 100 100 100)))
      (equal (pixelLessThanThreshold pixel threshOld) t)))
  
    (defproperty test-processThreshold :repeat 1000
    (a :value (random-integer)
       :where (< a 205)
       b :value (random-integer)
         :where (< b 205)
         c :value (random-integer)
           :where (< c 205))
    (let ((pixel (createRGB a b c)))
      (equal (car (getPixel (processThreshold (insertPixel *tree4* 2 1 a b c) pixel 1 *height* *width* *height*) 2 1)) 255)))
  
    (defproperty test-MainThreshold :repeat 1000
    (a :value (random-integer)
       :where (< a 120)
       b :value (random-integer)
         :where (< b 120)
         c :value (random-integer)
           :where (< c 120))
    (let ((pixel (createRGB a b c)))
      (equal (car (getPixel (MainThreshold (insertPixel *tree4* 2 1 a b c) 120 120 120) 2 1)) 255))))
  
  
  (link RTThreshold
        (MCommon MImage MThreshold TThreshold))
  
  
  (invoke RTThreshold)